Feat/Opcode Circuits for DIV, REM, and REMU opcodes #596

bgillesp · 2024-11-18T15:05:24Z

This PR extends the existing DIVU opcode implementation to expose the remainder as an output, and to handle the (more complicated) signed case. See the comments in div.rs for details, but in summary:

The basic design of signed and unsigned DIV and REM opcode circuits is to represent the division algorithm relation dividend = quotient * divisor + remainder using native field elements, and constraining so that either 0 <= remainder < divisor or divisor == 0 holds.
Some nontrivial steps are needed in the signed case to handle the additional complexity of different signs for the divisor and remainder values, as well as to handle signed division overflow where -2^31 / -1 = 2^31 is out of the representable range for i32 values.
In either case, either the quotient or the remainder value is exposed as the output register rd.
In theory with the current implementation, consecutive calls to DIV and REM or DIVU and REMU could be batched into a single circuit since both of the outputs are represented; however, this is not yet implemented.

Currently the circuit implementation and documentation are finished and ready for review. Unit tests still need to be finished, but it would be great to get some eyes on the circuit design now.

kunxian-xia · 2024-12-10T02:17:49Z

@bgillesp when will this pr be ready for review?

bgillesp · 2024-12-10T16:25:37Z

Unit tests still need to be added for the new opcode circuits, but everything else is in shape for an initial review -- will change the PR out of Draft now.

Implementing a TODO from #596

matthiasgoergens · 2024-12-11T01:35:49Z

ceno_zkvm/src/gadgets/is_lt.rs

@@ -18,6 +18,7 @@ use crate::{

 use super::SignedExtendConfig;

+// TODO rename to AssertLtConfig (LT -> Lt) to fit naming conventions


To help make #596 easier to read and reason about.

To make the diff for #596 easier to read.

matthiasgoergens

A few comments and suggestions so far.

ceno_zkvm/src/gadgets/signed.rs

ceno_zkvm/src/gadgets/signed_ext.rs

matthiasgoergens · 2024-12-11T01:45:29Z

ceno_zkvm/src/instructions/riscv/div.rs

Please merge #733 first, so that we can read the diff here better. Thanks!

You can solve any conflicts by just using your version of the code, because that's what we are trying to do here. You can either do that manually or via something like git merge --strategy recursive --strategy-option=ours origin/master

See https://github.com/scroll-tech/ceno/pull/734/files#diff-44194ded9672e9ed47ef78c46573cc0860f9317811d6be41b259afb554a989b4 for how that minimises and simplifies the diff.

#733 is merged.

Finished merging in master, hopefully the diff is a little nicer now.

To make the diff for #596 easier to read.

matthiasgoergens · 2024-12-11T03:02:43Z

@bgillesp I made a version of this PR that has an easier to read diff and left some comments there. They apply here as well. See #734

hero78119 · 2024-12-11T03:06:42Z

Attach DIVU circuit statistics 🔥

First row master branch, second row this PR

+---------------+---------------+---------+-------+-----------+--------+------------+---------------------+
| opcode_name   | num_instances | lookups | reads | witnesses | writes | 0_expr_deg | 0_expr_sumcheck_deg |
+---------------+---------------+---------+-------+-----------+--------+------------+---------------------+
| DIVU          | 0             | 21      | 4     | 37        | 4      | [1: 7]     | [2: 8]              | 
| DIVU          | 0             | 13      | 4     | 29        | 4      | [1: 5]     | [2: 5]              |

matthiasgoergens · 2024-12-11T03:17:54Z

Attach DIVU circuit statistics 🔥

First row master branch, second row this PR

+---------------+---------------+---------+-------+-----------+--------+------------+---------------------+
| opcode_name   | num_instances | lookups | reads | witnesses | writes | 0_expr_deg | 0_expr_sumcheck_deg |
+---------------+---------------+---------+-------+-----------+--------+------------+---------------------+
| DIVU          | 0             | 21      | 4     | 37        | 4      | [1: 7]     | [2: 8]              | 
| DIVU          | 0             | 13      | 4     | 29        | 4      | [1: 5]     | [2: 5]              |

Keep in mind that the PR has at least one bug (and that might affect the stats)?

ceno_zkvm/src/instructions/riscv/div.rs

KimiWu123 · 2024-12-11T06:19:34Z

ceno_zkvm/src/gadgets/signed.rs

+        &self,
+        instance: &mut [MaybeUninit<E::BaseField>],
+        lkm: &mut LkMultiplicity,
+        val: &Value<u32>,


Will it be better to use i32? Callers could assign i32::MAX + 1, and this could cause unexpeced result If the type isu32.

I think this might be a nontrivial change to implement -- the Value type seems to lean into the design of an "unsigned integer register" which can be interpreted as signed as desired, but not by default. In particular, the generic type T for Value<T> is currently constrained to Into<u64> + From<u32>, so u32 and u64 values are first-class citizens, but things break when I try to make it an i32. The gadget is really designed to provide a signed interpretation to an unsigned register value anyway, so I think that's why I originally chose the u32 representation. Okay if we leave it as is for now?

ceno_zkvm/src/instructions/riscv/div.rs

hero78119

Epic job! thanks for the implementation and clear documentation.
Just do a quick overview and will proceed arithmetics constrain review 2nd round

ceno_zkvm/src/gadgets/signed_ext.rs

ceno_zkvm/src/gadgets/signed.rs

ceno_zkvm/src/instructions/riscv/div.rs

…opcodes The current implementation tries to be generic over different UInt widths, but the circuit design soundness relies on specifically using 32-bit registers in the Goldilocks field, so it doesn't make sense to sacrifice readability for unused generality here.

…lity

…tion

… versions

…ded value The current assumption of the circuit design is that n_bits has to be 8 or 16, so this change will better flag violations of this assumption if we end up changing the base limb size to 32 bits.

bgillesp · 2024-12-11T18:13:38Z

Thank you for the generous feedback everyone! 🙏 I think I've addressed your comments as much as I can currently -- will keep an eye on this space to help move things forward as the review progresses.

To help make #596 easier to read and reason about. Also introduce a few more conversion helpers.

KimiWu123 · 2024-12-12T02:39:52Z

ceno_zkvm/src/instructions/riscv/div.rs

+                let neg_div_expr = {
+                    let a_neg = dividend_signed.is_negative.expr();
+                    let b_neg = divisor_signed.is_negative.expr();
+                    &a_neg * (1 - &b_neg) + (1 - &a_neg) * &b_neg


Really minor one, I like the original style more because It's clear and slightly efficient. It reduces the number of recursion here. But it depends on you :)

// a_neg * (1 - b_neg) + (1 - a_neg) * b_neg (a_neg.clone() + b_neg.clone()) - (Expression::<E>::from(2) * a_neg * b_neg)

Yeah, I think the fact that it was simplified to monomial form was why I went with the original version, but then the current revision is closer to the underlying logic of the expression, which gives an easily readable meaning for binary inputs. I don't think I have a strong opinion about it -- any thoughts @matthiasgoergens since the change was your suggestion?

There are two parts to my suggestion. One is to remove the manual clones, and the other is to use a simpler algebraic expression.

They are independent of each other.

I don't really have much of an opinion on whether (a + b - 2 * a * b) or a * (1 - b) + (1 - a) * b is easier to read. I went with the latter, because someone had made a comment // a_neg * (1 - b_neg) + (1 - a_neg) * b_neg to that end; so I assume someone thought that form is easier to read.

Here's my suggestion, if you want to use the original expression:

// a_neg xor b_neg &a_neg + &b_neg - 2 * a_neg * b_neg

Btw, when you say 'efficient', do you mean that the distribution function will be called slightly less often; or do you mean that the final resulting expression will be different?

Sure, this seems also like a good way to write it, with the simple comment -- updated to this version in the latest commit.

KimiWu123 · 2024-12-12T02:40:52Z

ceno_zkvm/src/instructions/riscv/div.rs


        Ok(())
    }
 }

+// TODO Tests


I guess you forgot this TODO. I didn't see any testing added.

Not forgotten! I mentioned that this is still TODO in the PR description -- another member of our team is working on it, but paused yesterday due to the rapid changes from the review. Should be finished relatively soon, but probably an initial review of the circuit design would still be valuable at this point before we validate with unit tests.

Implementing a TODO from #596

To make the diff for scroll-tech#596 easier to read.

To help make scroll-tech#596 easier to read and reason about. Also introduce a few more conversion helpers.

Implementing a TODO from scroll-tech#596

bgillesp · 2024-12-13T18:45:24Z

Note that while commit e719763 is showing failed tests, the cargo make tests command runs successfully on my local build, so I'm guessing it might be something stalled on the CI end.

Bryan Gillespie added 2 commits November 15, 2024 11:34

Move Signed gadget from MULH opcode to gadgets submodule

4fb46a4

Extend DIVU gadget implementation to support REMU/DIV/REM opcodes

2812c12

This was linked to issues Nov 19, 2024

remu #590

Open

div #588

Open

rem #589

Open

mcalancea self-assigned this Dec 6, 2024

Bryan Gillespie added 6 commits December 6, 2024 13:36

Format updates

6919ece

Merge branch 'master' into bg/div-rem-remu-opcodes

754a75d

A few DIV opcode circuit fixes, documentation, and vm integration

b9be2fc

Rename divu.rs to div.rs and add check for Goldilocks field

22bc22a

Small reformatting and doc improvements

4c11b43

Merge branch 'master' into bg/div-rem-remu-opcodes

277fd77

kunxian-xia requested a review from naure December 10, 2024 02:17

bgillesp changed the title ~~[WIP] Feat/Opcode Circuits for DIV, REM, and REMU opcodes~~ Feat/Opcode Circuits for DIV, REM, and REMU opcodes Dec 10, 2024

bgillesp marked this pull request as ready for review December 10, 2024 16:25

Bryan Gillespie added 2 commits December 10, 2024 09:38

Formatting fix

36c2af4

Fix a couple of missed changes in rv32im.rs needed for new opcodes

3e7931b

matthiasgoergens added a commit that referenced this pull request Dec 11, 2024

Rename AssertLTConfig to AssertLtConfig

9878cc8

Implementing a TODO from #596

matthiasgoergens mentioned this pull request Dec 11, 2024

Rename AssertLTConfig to AssertLtConfig #731

Merged

matthiasgoergens reviewed Dec 11, 2024

View reviewed changes

matthiasgoergens added a commit that referenced this pull request Dec 11, 2024

Introduce Value::as_i32

ed6797b

To help make #596 easier to read and reason about.

matthiasgoergens mentioned this pull request Dec 11, 2024

Introduce Value::as_i32 #732

Merged

matthiasgoergens added a commit that referenced this pull request Dec 11, 2024

Rename mod divu to mod div

0af1111

To make the diff for #596 easier to read.

matthiasgoergens mentioned this pull request Dec 11, 2024

Rename mod divu to mod div #733

Merged

matthiasgoergens reviewed Dec 11, 2024

View reviewed changes

kunxian-xia pushed a commit that referenced this pull request Dec 11, 2024

Rename mod divu to mod div (#733)

a879b84

To make the diff for #596 easier to read.

KimiWu123 reviewed Dec 11, 2024

View reviewed changes

hero78119 reviewed Dec 11, 2024

View reviewed changes

ceno_zkvm/src/gadgets/signed_ext.rs Show resolved Hide resolved

ceno_zkvm/src/gadgets/signed.rs Outdated Show resolved Hide resolved

ceno_zkvm/src/instructions/riscv/div.rs Outdated Show resolved Hide resolved

Bryan Gillespie added 15 commits December 11, 2024 07:39

Fix bug in signed remainder construction

7821de4

Small comment fixes

23e6421

Update UInt assignment in DIV opcodes to use assign_value function

eb0a117

Change unnecessary generic constant with hard-coded value for readabi…

4425c13

…lity

Merge branch 'master' into bg/div-rem-remu-opcodes

0158e01

Change Signed circuit to use bit shift directly on expression

54bf10c

Small updates based on PR comments

92bce79

Fix assignment to remainder_nonnegative in DIV/REM opcodes circuit

8317a28

Simplify syntax for a few Expression definitions

0c3f5ed

Remove a few unnecessary type annotations

41e3e19

Use built-in arithmetic calls for unsigned quotient/remainder computa…

137964a

…tion

Simplify variables in signed DIV/REM assignment by shadowing unsigned…

0f71c30

… versions

Use parameter for limb size in SignedExtendConfig rather than hard-co…

124d623

…ded value The current assumption of the circuit design is that n_bits has to be 8 or 16, so this change will better flag violations of this assumption if we end up changing the base limb size to 32 bits.

Revise Signed val construction to use relevant UInt utility function

833dbca

matthiasgoergens added a commit that referenced this pull request Dec 12, 2024

Introduce Value::as_i32 (#732)

2cd6a6d

To help make #596 easier to read and reason about. Also introduce a few more conversion helpers.

KimiWu123 reviewed Dec 12, 2024

View reviewed changes

Merge branch 'master' into bg/div-rem-remu-opcodes

5947d99

matthiasgoergens added a commit that referenced this pull request Dec 12, 2024

Rename AssertLTConfig to AssertLtConfig (#731)

35b352e

Implementing a TODO from #596

10to4 pushed a commit to 10to4/ceno that referenced this pull request Dec 12, 2024

Rename mod divu to mod div (scroll-tech#733)

cf15c14

To make the diff for scroll-tech#596 easier to read.

10to4 pushed a commit to 10to4/ceno that referenced this pull request Dec 12, 2024

Introduce Value::as_i32 (scroll-tech#732)

e28e557

To help make scroll-tech#596 easier to read and reason about. Also introduce a few more conversion helpers.

10to4 pushed a commit to 10to4/ceno that referenced this pull request Dec 12, 2024

Rename AssertLTConfig to AssertLtConfig (scroll-tech#731)

5077eb1

Implementing a TODO from scroll-tech#596

Bryan Gillespie added 2 commits December 13, 2024 10:31

Merge branch 'master' into bg/div-rem-remu-opcodes

19647e0

Change way that expression for neg_div_expr is written

e719763

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feat/Opcode Circuits for DIV, REM, and REMU opcodes #596

Feat/Opcode Circuits for DIV, REM, and REMU opcodes #596

bgillesp commented Nov 18, 2024 •

edited

Loading

kunxian-xia commented Dec 10, 2024

bgillesp commented Dec 10, 2024

matthiasgoergens Dec 11, 2024

matthiasgoergens left a comment

matthiasgoergens Dec 11, 2024

kunxian-xia Dec 11, 2024

bgillesp Dec 11, 2024

matthiasgoergens commented Dec 11, 2024

hero78119 commented Dec 11, 2024 •

edited

Loading

matthiasgoergens commented Dec 11, 2024 •

edited

Loading

KimiWu123 Dec 11, 2024

bgillesp Dec 11, 2024

hero78119 left a comment

bgillesp commented Dec 11, 2024

KimiWu123 Dec 12, 2024

bgillesp Dec 12, 2024

matthiasgoergens Dec 12, 2024 •

edited

Loading

bgillesp Dec 13, 2024

KimiWu123 Dec 12, 2024

bgillesp Dec 12, 2024

bgillesp commented Dec 13, 2024

		@@ -18,6 +18,7 @@ use crate::{

		use super::SignedExtendConfig;

		// TODO rename to AssertLtConfig (LT -> Lt) to fit naming conventions

Feat/Opcode Circuits for DIV, REM, and REMU opcodes #596

Are you sure you want to change the base?

Feat/Opcode Circuits for DIV, REM, and REMU opcodes #596

Conversation

bgillesp commented Nov 18, 2024 • edited Loading

kunxian-xia commented Dec 10, 2024

bgillesp commented Dec 10, 2024

Choose a reason for hiding this comment

matthiasgoergens left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

matthiasgoergens commented Dec 11, 2024

hero78119 commented Dec 11, 2024 • edited Loading

matthiasgoergens commented Dec 11, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hero78119 left a comment

Choose a reason for hiding this comment

bgillesp commented Dec 11, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

matthiasgoergens Dec 12, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bgillesp commented Dec 13, 2024

bgillesp commented Nov 18, 2024 •

edited

Loading

hero78119 commented Dec 11, 2024 •

edited

Loading

matthiasgoergens commented Dec 11, 2024 •

edited

Loading

matthiasgoergens Dec 12, 2024 •

edited

Loading